@incollection{Cousot81-1-MuchnickJones,
   author =    {Cousot, P{.}},
   title =     {Semantic Foundations of Program Analysis},
   pages =     {303--342},
   editor =    {Muchnick, S.S{.} and Jones, N.D{.}},
   chapter =   10,
   booktitle = {Program Flow Analysis: Theory and Applications},
   publisher = {Prentice\discretionary{-}{}{-}Hall},
   year =      1981,
 }
@InProceedings{CousotCousot77-3,
   author =    {Cousot, P{.} and Cousot, R{.}},
   title =     {Static determination of dynamic properties of recursive
                procedures},
   pages =     {237--277},
   editor =    {Neuhold, E.J{.}},
   booktitle = {IFIP Conf.\ on Formal Description of Programming Concepts},
   publisher = {North\discretionary{-}{}{-}Holland},
   year =      1977,
}
@phdThesis{Cousot78-1-TheseEtat,
   author =    {Cousot, P{.}},
   title =     {M{\'e}\-tho\-des it{\'e}\-ra\-ti\-ves de cons\-truc\-tion et
                d'ap\-pro\-xi\-ma\-tion de points fi\-xes
                d'op{\'e}\-ra\-teurs mo\-no\-to\-nes sur un treil\-lis,
                ana\-ly\-se s{\'e}\-man\-ti\-que de pro\-gram\-mes (in {F}rench)},
   school =    {Uni\-ver\-si\-t{\'e} scien\-ti\-fi\-que et
                m{\'e}\-di\-ca\-le de Gre\-no\-ble},
   type =      {Th{\`e}\-se d'{{\'E}}tat {\`e}s scie\-nces
                ma\-th{\'e}\-ma\-ti\-ques},
   year =      1978,
 }
   address =   {Gre\-no\-ble},
   month =     {21 March },
@InProceedings{Bourdoncle93-2,
   author =    {Bourdoncle, F{.}},
   title =     {Abstract Debugging of Higher-Order Imperative Languages},
   pages =     {46--55},
   booktitle = {PLDI$\,$'93},
   publisher = {ACM},
   year =      1993,
}
   month =     {23--25 June },
   address =   {Albuquerque},
@incollection{Bourdoncle93-3,
   author =    {Bourdoncle, F{.}},
   title =     {Assertion-Based Debugging of Imperative Programs by Abstract Interpretation},
   booktitle = {ESEC$\,$'{93}},
   series =    {LNCS  717},
   pages =     {501--516},
   year =      1993,
   publisher = {Springer},
}
   editor =    {I{.} Sommerville and M{.} Paul},
@InProceedings{CousotCousot77-1-POPL,
   author =    {Cousot, P{.} and Cousot, R{.}},
   title =     {Abstract interpretation: a unified lattice model for static
                analysis of programs by construction or approximation of
              fixpoints},
   pages =     {238--252},
   booktitle = {4$^{\mathrm{th}}$  POPL},
   publisher = {ACM},
   year =      1977,
}
   address =   {Los Angeles},
@InProceedings{CousotCousot79-1-POPL,
   author =    {Cousot, P{.} and Cousot, R{.}},
   title =     {Systematic design of program analysis frameworks},
   pages =     {269--282},
   booktitle = {6$^{\mathrm{th}}$  POPL},
   publisher = {ACM},
   year =      1979,
}
   address =   {San Antonio},
@inproceedings{FerraraLogozzoFahndrich-OOPSLA08,
  author = {P{.} Ferrara and F{.} Logozzo and M{.} F{\"a}hndrich},
  title  = {Safer Unsafe Code in .{NET}},
  booktitle = {OOPSLA'08},
  year    = 2008,
  publisher = {ACM},
}
%  address =   {Nashville, USA},
%  booktitle = {Proceedings of the {ACM} Conference on Object-Oriented Programming, Systems, Languages and Applications},
@book{eiffel,
   author =    {B.~Meyer},
   title =     {Eiffel: The Language},
   publisher = {Prentice Hall},
   year =      1991,
}
@inproceedings{CousotCousotLogozzo-09,
   author = {P{.}~Cousot and R{.}~Cousot and F{.}~Logozzo},
   title  = {A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis},   
   booktitle = {POPL$\,$'2011},
   publisher = {ACM Press},
   year =      2011,
}
@techReport{CousotCousotLogozzo-10,
   author = {P{.}~Cousot and R{.}~Cousot and F{.}~Logozzo},
   title  = {Contract Precondition Inference from Intermittent Assertions on Collections},   
   institution = {MSR-TR-2010-117, MSR Redmond},
   month = sep,
   year = 2010,
}
@article{Cousot02-TCS,
   author =    {Cousot, P{.}},
   title =     {Constructive Design of a Hierarchy of Semantics of a
                Transition System by Abstract Interpretation},
   journal =   {TCS},
   volume =    277,
   number =    {1---2},
   pages =     {47--103},
   year =      2002,
}
@article{AlpernSchneider-IPL85,
   author =  {B{.} Alpern and F{.}B{.} Schneider},
   title =   {Defining Liveness},
   journal = {IPL},
   volume = 21,
   pages = {181--185},
   year =    1985,
}
@incollection{BiereEtAl-DAC99,
   author =    {Biere, A{.} and Cimatti, A{.} and Clarke, E.M{.} and Fujita, M{.}
                and Zhu, Y{.}},
   title =     {Symbolic Model Checking Using {SAT} Procedures instead of {BDD}s},
   booktitle = {DAC$\,$'{99}},
   year =      {1999},
   publisher = {ACM},
   pages =     {317--320},
}
   series =    {New Orleans},
@article{BiereEtAl03-BMC,
   author =  {Biere, A{.} and Cimatti, A{.} and Clarke, E.M{.} and
                Strichman, O{.} and Zhu, Y{.}},
   title =   {Bounded Model Checking},
   journal = {Advances in Computers},
   volume =  58,
   pages =   {118--149},
   year =    2003,
}
@inproceedings{ClarkeEtAl92-1,
   author =    {Clarke, E.M{.} and Grumberg, O{.} and Long, D.E{.}},
   title =     {Model Checking and Abstraction},
   booktitle = {POPL$\,$'92},
   publisher = {ACM},
   year =      1992,
   pages =     {343--354},
}
   address =   {Albuquerque},
@inCollection{GoubaultPutot-SAS07,
   author =    {{\'E}{.}~Goubault and S{.}~Putot},
   title =     {Under-Approximations of Computations in Real Numbers Based on Generalized Affine Arithmetic},
   booktitle = {SAS$\,$'{07}},
   year =      2007,
   series =    {LNCS  4634},
   publisher = {Springer},
   pages =     {137--152},
}
   editor =    {Fil\'e, G{.} and Riis-Nielson, H{.}},
   month =     {22--24 August },
@inproceedings{GulwaniMcCloskeyTiwari-POPL08,
   author =    {S{.}~Gulwani and B{.}~McCloskey and A{.}~Tiwari},
   title =     {Lifting Abstract Interpreters to Quantified Logical Domains},
   pages =     {235--246},
   booktitle = {POPL$\,$'08},
   publisher = {ACM},
   year =      2008,
}
   address =   {San Francisco, California},
   editor = {G{.}C{.}~Necula and P{.}~Wadler},
   month =     {7--12 January },
@inproceedings{LandiRyder-POPL91,
   author =    {W{.}~Landi and B{.}G{.}~Ryder},
   title =     {Pointer-Induced Aliasing: A Problem Classification},
   pages =     {93--103},
   booktitle = {POPL$\'$91},
   publisher = {ACM},
   year =      1991,
}
   address =   {Orlando, Florida},
   month =     {7--12 January},
@article{Schmidt-SCP07,
   author =  {D{.}A{.}~Schmidt},
   title =   {A calculus of logical relations for over- and underapproximating static analyses},
   journal = {SCP},
   volume =  64,
   number =  1,
   pages =   {29--53},
   year =    2007,
}
   month =   {January},
@unpublished{ErezYahavSagiv-94,
   author =  {G{.}~Erez and E{.}~Yahav and M{.}~Sagiv},
   title =   {Generating Concrete Counterexamples for Sound Abstract Interpretation},
   note =   {Unpublished Manuscript},
   year =    1994,
}      
@techReport{Pratt77-1,
   author =      {V.R{.} Pratt},
   title =       {Two Easy Theories Whose Combination is Hard},
   institution = {MIT},
   year =        1977,
   note = {\url{boole.stanford.edu/pub/sefnp.pdf}},
}
%   month = {september  1,},
@article{Roy59-CRAS,
   author =  {B{.} Roy},
   title =   {Transitivit{\'e} et connexit{\'e}},
   journal = {Comptes\discretionary{-}{}{-}Rendus de l'Acad{\'e}mie des Sciences de Paris, S{\'e}r{.} A-B},
   volume =  249,
   pages =   {216--218},
   year =    1959,
}
@article{Shostak81-JACM,
   author =  {R{.} Shostak},
   title =   {Deciding Linear Inequalities by Computing Loop Residues},
   journal = {JACM},
   volume =  28,
   number =  4,
   pages =   {769--779},
   year =    1981,
}
@inproceedings{Dill89-1,
   author =    {Dill, D.L{.}},
   title =     {Timing assumptions and verification of finite-state concurrent
                systems},
   booktitle = {Automatic Verification Methods for Finite State Systems},
   series =    {LNCS  407},
   publisher = {Springer},
   pages =     {197--212},
   year =      1989,
}
@article{Mine-HOSC06,
   author =    {Min\'e, A{.}},
   title =   {The Octagon Abstract Domain},
   journal = {Higher-Order and Symbolic Computation},
   volume = 19,
   pages = {31--100},
   year =    2006,
}
@article{Tarski55-1,
   author =   {Tarski, A{.}},
   title =    {A lattice theoretical fixpoint theorem and its applications},
   journal =  {Pacific Journal of Mathematics},
   year =     1955,
   volume =   5,
   pages =    {285--310},
}
@InProceedings{CousotHalbwachs78-1-POPL,
   author =    {Cousot, P{.} and Halbwachs, N{.}},
   title =     {Automatic discovery of linear restraints among variables of a
                program},
   pages =     {84--97},
   booktitle = {POPL$\,$78},
   publisher = {ACM},
   year =      1978,
}
   address =   {Tucson},
@incollection{CousotCousot82-2-TNCP,
   author =    {Cousot, P{.} and Cousot, R{.}},
   title =     {Induction principles for proving invariance properties of
                programs},
   pages =     {43--119},
   editor =    {N{\'e}el, D{.}},
   booktitle = {Tools \& Notions for Program Construction},
   publisher = {Cambridge University Press},
   year =      1982,
}
@phdthesis{CousotR85-1,
   author =  {Cousot, R{.}},
   title =   {Fon\-de\-ments des m{\'e}\-tho\-des de preu\-ve
              d'in\-va\-rian\-ce et de fa\-ta\-li\-t{\'e} de pro\-gram\-mes
              pa\-ral\-l{\`e}\-les (in {F}rench)},
   school =  {Ins\-ti\-tut na\-tio\-nal po\-ly\-tech\-ni\-que de Lor\-rai\-ne},
   type =    {Th{\`e}\-se d'{{\'E}}tat {\`e}s scien\-ces
              ma\-th{\'e}\-ma\-ti\-ques, Nan\-cy},
   year =    1985,
}
   month =   {15 November },
@incollection{CousotCousot85-1-AMS,
   author =    {Cousot, P{.} and Cousot, R{.}},
   title =     {`{{\`A}} la {F}loyd' induction principles for proving
                inevitability properties of programs},
   pages =     {277--312},
   chapter =   8,
   booktitle = {Algebraic Methods in Semantics},
   publisher = {Cambridge University Press},
   year =      1985,
}
   editor =    {Nivat, M{.} and Reynolds, J{.}},
@InProceedings{BarnettFahndrichLogozzo-SAC-2010,
   author =    {M{.}~Barnett and M{.}~F{\"a}hndrich and F{.}~Logozzo},
   title =     {Embedded Contract Languages},
   pages =     {2103--2110},
   booktitle = {SAC'10},
   publisher = {ACM},
   year =      2010,
}
   editor =    {S{.}Y{.}~Shin and S{.}~Ossowski and M{.}~Schumacher and M{.}J{.}~Palakal and C{.}-C{.}~Hung},
   address =   {Sierre, Switzerland},
   month =     {March 22--26},
@article{Dijkstra75-1,
   author =  {Dijkstra, E.W{.}},
   title =   {Guarded Commands, Nondeterminacy and Formal Derivation of
              Programs},
   journal = {CACM},
   year =    1975,
   volume =  18,
   number =  8,
   pages =   {453--457},
}
   month =   {August },
@inCollection{Cousot99-3-Marktoberdorf-paper,
   author =    {Cousot, P{.}},
   title =     {The Calculational Design of a Generic Abstract
                Interpreter},
   booktitle = {Calculational System Design},
   editor =    {M{.} Broy and R{.} Steinbr{\"u}ggen},
   publisher = {{NATO} Science Series, Series F: Computer and Systems
                Sciences. IOS Press},
   volume =    173,
   pages =     {421--505},
   year =      1999,
}
   publisher = {{NATO} Science Series, Series F: Computer and Systems
                Sciences. IOS Press, Amsterdam},
@book{BaierKatoen08-POMC,
   author =    {Baier, C{.} and Katoen, J.-P{.}},
   title =     {Principles of Model Checking},
   publisher = {MIT Press},
   year =      2008,
}
   address =   {Cambridge},
@article{CousotCousot92-2-JLP,
   author =  {Cousot, P{.} and Cousot, R{.}},
   title =   {Abstract Interpretation and Application to Logic Programs},
   pages =   {103--179},
   journal = {Journal of Logic Programming},
   year =    1992,
   volume =  13,
   number =  {2--3},
   note =    {\iflong\footnote{\tiny (The editor of Journal of Logic Programming{} has mistakenly published the
              unreadable galley proof. For a correct version of this paper, see
              \url{http://www.di.ens.fr/~cousot}.)}\fi},
}
@book{Hecht-DFA77,
   author =    {M{.}S{.}\ Hecht},
   title =     {Flow Analysis of Computer Programs},
   publisher = {Elsevier North-Holland},
   year =      1977,
}
@inproceedings{Schmidt98-1,
   author =    {Schmidt, D.A{.}},
   title =     {Data-flow analysis is model checking of abstract interpretations},
   pages =     {38--48},
   booktitle = {POPL$\,$98},
   publisher = {ACM},
   year =      1998,
}
   address =   {San Diego},
   MONTH     = {19--21 January },
@techReport{Lev-AmiSagivRepsGulwani07-pre,
   author =      {T{.}Lev-Ami and M{.} Sagiv and T{.} Reps	and S{.} Gulwani},
   title =       {Backward Analysis for Inferring Quantified Preconditions},
   type = {TR-2007-12-01},
   institution = {Tel Aviv University},
   year =        2007,
}
@article{ArnoutMeyer03-HiddenContracts,
   author =  {K{.} Arnout and B{.} Meyer},
   title =   {Uncovering Hidden Contracts: The .{NET} Example},
   journal = {IEEE Computer},
   volume =  36,
   number =  11,
   pages =   {48--55},
   year =    2003,
}   
@article{Meyer92-DbC,
   author =  {B{.} Meyer},
   title =   {{Applying ``Design by Contract''}},
   journal = {IEEE Computer},
   volume =  25,
   number =  10,
   pages =   {40--51},
   year =    1992,
}
   month =   {Oct.},
@inproceedings{MoyY-VMCAI08,
   author =    {Moy, Y{.}},
   title =     {Sufficient Preconditions for Modular Assertion Checking},
   pages =     {188--202},
   booktitle = {VMCAI$\,$08},
   series =    {LNCS 4905},
   publisher = {Springer},
   year =      2008,
}
@inCollection{Rival-SAS05,
   author =    {X{.}~Rival},
   title =     {Understanding the origin of alarms in \textsc{Astr\'ee}},
   booktitle = {SAS$\,$'{05}},
   year =      2005,
   series =    {LNCS  3672},
   publisher = {Springer},
   pages =     {303--319},
}
@inCollection{GulwaniTiwari-ESOP07,
   author =    {S{.}~Gulwani and A{.}~Tiwari},
   title =     {Computing Procedure Summaries for Interprocedural Analysis},
   booktitle = {ESOP$\,$'{07}},
   year =      2007,
   series =    {LNCS  4421},
   publisher = {Springer},
   pages =     {253--267},
}
@article{King-CACM76,
   author =  {J{.}C{.}~King},
   title =   {Symbolic Execution and Program Testing},
   journal = {CACM},
   volume =  19,
   number =  7,
   pages =   {385--394},
   year =    1976,
}
   month =   {July},
@inCollection{BarnettEtAl-IWACO07,
   author =    {M{.}~Barnett and M{.}~F{\"a}hndrich and D{.}~Garbervetsky and F{.}~Logozzo},
   title =     {Annotations for (more) Precise Points-to Analysis},
   booktitle = {IWACO$\,$'{07}},
   publisher = {Stockholm U.\ and KTH},
   year =      2007,
}
   series =    {DSV Report series No{.}~07-010},
   pages =     {???},
   publisher = {Department of Computer and Systems Sciences at Stockholm University and KTH.
@article{ErnstEtAl07-DAIKON,
   author =  {M{.}D{.}~Ernst and J{.}H{.}~Perkins and P{.}J{.}~Guo and S{.}~McCamant and C{.}~Pacheco and M{.}S{.}~Tschantz and C{.}~Xiao},
   title =   {The Daikon system for dynamic detection of likely invariants},
   journal = {Sci. Comput. Program.},
   volume =  69,
   number =  {(1-3)},
   pages =   {35-45},
   year =    2007,
}
   month =   {•},
@article{LeeEtAL05-testing,
   author =  {G{.}~Lee and J{.}~Morris and K{.}~Parker and G{.}A{.}~Bundell and C{.}P{.}~Lam},
   title =   {Using symbolic execution to guide test generation},
   journal = {Software Testing, Verification \& Reliability},
   volume =  15,
   number =  1,
   pages =   {41--61},
   year =    2005,
}  
   month =   {•},
@inproceedings{MafLogozzo10,
 author = {M{.}~F\"{a}hndrich and F{.}~Logozzo},
 title = {Clousot: {S}tatic contract checking with Abstract Interpretation},
 booktitle = {FoVeOOS},
 year = {2010},
 location = {Paris, France},
 publisher = {Springer},
 }
  booktitle = {FoVeOOS: Conference on Formal Verification of Object-Oriented software},
 @inproceedings{ChandraFinkSridharan09-PLDI,
 author = {S{.}~Chandra and S{.}J{.}~Fink and M{.}~Sridharan},
 title = {Snugglebug: a powerful approach to weakest preconditions},
 booktitle = {PLDI},
 year = {2009},
 pages = {363--374},
 location = {Dublin, Ireland},
 publisher = {ACM},
 }
 @inproceedings{FlanaganEtAL02-PLDI,
 author = {C{.}~Flanagan and K{.}R{.}M{.}~Leino and M{.}~Lillibridge and G{.}~Nelson and J{.}B{.}~Saxe and R{.}~Stata},
 title = {{Extended Static Checking for Java}},
 booktitle = {PLDI},
 year = {2002},
 pages = {234--245},
 location = {Berlin, Germany,},
 publisher = {ACM},
 }
 @inproceedings{CousotCousot-CC02,
   author =  {P{.} Cousot and R{.} Cousot},
   title = {Modular Static Program Analysis},
   pages =     {159--178},
   booktitle = {CC 2002},
   address =   {Grenoble, France},
   publisher = {LNCS 2304, Springer},
   year =      2002,
}
   editor =    {Horspool, R.N{.}},'
      booktitle = {Proceedings of the Eleventh International Conference on
                Compiler Construction (CC 2002)},
   month =     {April 6---14},
@InProceedings{CalcagnoEtAl-POPL09,
   author =    {C{.}~Calcagno and D{.}~Distefano and P{.}W{.}~O'Hearn and H{.}~Yang},
   title =     {Compositional shape analysis by means of bi-abduction},
   pages =     {289--300},
   booktitle = {36$^{\mathrm{th}}$  POPL},
   publisher = {ACM},
   year =      2009,
}
 Zhong Shao, Benjamin C. Pierce (Eds.): Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009. ACM 2009, ISBN 978-1-60558-379-2   
 @incollection{Park69-FxpInd,
   author =    {Park, D{.}},
   title =     {Fixpoint induction and proofs of program properties},
   pages =     {59--78},
   editor =    {B.~Meltzer and D.~Michie},
   booktitle = {Machine Intelligences},
   volume =    5,
   publisher = {Edinburgh University Press},
   year =      1969,
 }

